Correctness conditions for concurrent objects describe how atomicity of anabstract sequential object may be decomposed. Many different concurrent objectsand proof methods for them have been developed. However, arguments aboutcorrectness are conducted with respect to an object in isolation. This is incontrast to real-world practice, where concurrent objects are often implementedas part of a programming language library (e.g., java.util.concurrent) and areinstantiated within a client program. A natural question to ask, then is: Howdoes a correctness condition for a concurrent object ensure correctness of aclient program that uses the concurrent object? This paper presents the mainissues that surround this question and provides some answers by linkingdifferent correctness conditions with a form of trace refinement.
展开▼
